Inference at * 
Iof proof for Lemma l before sublist:


  T:Type, L1, L2:(T List). L1  L2  {x, y:T. x before y  L1  x before y  L2} 

latex

 by ((((Unfolds ``l_before guard`` 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term)))) 
CollapseTHEN (Using [`L2',L1] Easy)) 

latex

C.

Definitions	t  T, x before y  l, {T}, P  Q, x:A. B(x),
Lemmas	sublist wf, sublist transitivity